Inference at * 2 1 
Iof proof for Lemma select nth tl:

.....truecase..... NILNIL

1. T : Type
2. T List
3. u : T
4. v : T List
5. n:{0...||v||}, i:{0..(||v|| - n)}. nth_tl(n;v)[i] = v[(i+n)]
6. n : {0...||v||+1}
7. i : {0..((||v||+1) - n)}
8. n  0
  [u / v][i] = [u / v][(i+n)] 

latex

 by ((Assert n = 0) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n
C)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 9. n = 0
C1:   [u / v][i] = [u / v][(i+n)]
C.

Definitions

t  T, False, P  Q, A, P & Q, i  j < k, A  B, {i..j}, {i...j}